$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, $k$:Knd, $x$:Id, $n$:$\mathbb{N}$, $f$:Top.
\\[0ex]update{-}spec{-}decl(update{-}spec1($k$;$x$;$n$;$s$,$v$.$f$($s$,$v$));${\it ds}$) $\Leftrightarrow$ $x$ $\in$ dom(${\it ds}$)